| 1: | app(app(,x),x) | → e | |
| 2: | app(app(,e),x) | → x | |
| 3: | app(app(,x),app(app(.,x),y)) | → y | |
| 4: | app(app(,app(app(/,x),y)),x) | → y | |
| 5: | app(app(/,x),x) | → e | |
| 6: | app(app(/,x),e) | → x | |
| 7: | app(app(/,app(app(.,y),x)),x) | → y | |
| 8: | app(app(/,x),app(app(,y),x)) | → y | |
| 9: | app(app(.,e),x) | → x | |
| 10: | app(app(.,x),e) | → x | |
| 11: | app(app(.,x),app(app(,x),y)) | → y | |
| 12: | app(app(.,app(app(/,y),x)),x) | → y | |